1. Field of the Invention
The present invention relates to the comparison of combinational circuits. More specifically, it relates to a method of comparing combinational circuits using Binary Decision Diagrams (BDDs), circuit graph hashing, cutpoint guessing, and false negative elimination.
2. Prior Art
In recent years, formal techniques for verifying properties of complex systems have become widely accepted in practical design methodologies. The computational complexity of the corresponding algorithms results in a fundamental trade-off between the generality of the verification model and the size of the designs that can be handled in practice. For example, verifying complex temporal properties using model checking is relatively expensive and often not scalable to designs with a large number of storage elements. Conversely, a combinational verification model significantly limits the expressiveness of the properties to be verified, but is practically applicable to large designs. Today, combinational models are commonly used to prove the functional equivalence of two design representations modeled on different levels of abstraction. The matching state encoding of the two models is enforced by the overall design methodology.
Most approaches to combinational circuit verification can be classified into two fundamental categories. The first category is based on functional implications computed directly on the circuit structure by applying algorithms for test pattern generation (ATPG) or recursive learning. The goal of these approaches is to prove that the XOR function between the two compared outputs cannot be justified to a logical "1". Starting at the primary inputs, the two circuits are successively merged, which typically simplifies the proof. The main problem with structure based approaches such as these, is the potentially large effort required to compute equivalence implications especially for circuits with no fine grain similarity. The search to find a pair of identical nets, which are further away from the primary inputs, can be very expensive.
The second category of approaches to combinational verification is based on canonical representations of Boolean functions, typically binary decision diagrams (BDDs) or their derivatives. The functions of the two circuits to be compared are converted into canonical forms which are then structurally compared. The major advantage of BDDs is their efficiency for a wide variety of practically relevant combinational circuits. If the BDD size does not grow too large, this type of Boolean reasoning is fast and independent of the actual circuit structure. Moreover, if structural similarities of the two designs are exploited, BDDs can effectively find equivalence implications between nets even if they are farther away from the primary inputs.
The primary problem with BDDs is their exponential memory complexity. If the BDD structure grows too large, their storage and manipulation effort becomes very expensive. Various approaches have been proposed to reduce the complexity of BDD-based equivalence checking by exploiting structural similarities. These techniques have been successful because a large majority of industrial designs contain many intermediate functions that occur in the specification and in the implementation. These nets can be used as cutpoints to partition a complex equivalence check into a set of smaller, simpler comparisons.
Most cutpoint-based verification methods consist of three phases. First, a set of potential cutpoints is identified by using random simulation, ATPG techniques, or BDDs. From these candidates the final cutpoints are chosen by specific selection criteria which are typically difficult to tune to a wider set of applications. Second, the overall verification task is partitioned along these cutpoints into a set of smaller verification problems which are solved independently. And third, in case of mis-compares, false negatives due to functional constraints at the partition boundaries are eliminated.
There are basically three methods to handle false negatives, all of which have fundamental limitations. The first method is based on resubstitution of the cutpoint variables by their incoming functions using the BDD compose operation. This method is extremely sensitive to the order in which the cutpoints are handled. In the worst case, a bad order might cause the elimination of all cutpoints including the ones which do not cause false negatives. Practically, the problem becomes more significant with more cutpoints since the likelihood of false negatives increases. This causes a dilemma for selecting the right number of cutpoints in that choosing too few results in a blow up of the forward BDD construction (i.e., exponential increase in memory demand), and choosing too many leads to an explosion of the resubstitution.
The second method for handling false negatives is based on cut frontiers, defined by the topological order of the cutpoints in the two networks. False negatives are eliminated by successively applying the image of the previous cut frontier to constrain the miscompare function of the current cut frontier. This method is basically identical to the backward traversal technique for sequential FSM verification and therefore has similar limitations (i.e, the size of the BDD representation of the image tends to blow up in many practical cases).
The third method for eliminating false negatives is based on ATPG techniques to disprove each counter example individually. Here the complexity has shifted into the time domain which makes the approach impractical if the set of miscomparing patterns is large. In addition, if the cutpoints are farther away from the primary inputs and no other functional implications between the two circuits are known, this technique might timeout even on individual counter examples.